The present invention relates generally to design automation and verification, and specifically to producing counterexamples in symbolic model checking.
Model checking is a method of formal verification that is gaining in popularity as a tool for use in designing complex systems, such as integrated circuits. The method is described generally by Clarke et al. in Model Checking (MIT Press, 1999), which is incorporated herein by reference.
To perform model checking of the design of a device, a user reads the definition and functional specifications of the device and then, based on this information, writes a set of properties {xcfx86} (also known as a specification) that the design is expected to fulfill. The properties are written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. Such languages are commonly based on Computation Tree Logic (CTL). A hardware model M (also known as an implementation) of the design, which is typically written in a hardware description language, such as VHDL or Verilog, is then tested to ascertain that the model satisfies all of the properties in the set, i.e., that M |=xcfx86, under all relevant input sequences.
One of the most useful features of model checking is its ability, when a property xcfx86 is found to be false on M, to construct a sequence of states and transitions (a path) that leads to the problematic state of the design. This path is called a counterexample. It can be used by the engineer in understanding and remedying the design defect that led to the failure of the model.
Model checking is preferably carried out automatically by a symbolic model checking program, such as SMV, as described, for example, by McMillan in Symbolic Model Checking (Kluwer Academic Publishers, 1993), which is incorporated herein by reference. A number of practical model checking tools are available, among them RuleBase, developed by IBM Corporation. This tool is described by Beer et al. in xe2x80x9cRuleBase: an Industry-Oriented Formal Verification Tool,xe2x80x9d in Proceedings of the Design Automation Conference DACxe2x80x296 (Las Vegas, Nev., 1996), which is incorporated herein by reference.
Symbolic CTL model checking, as described by McMillan, involves computing the transition-relation (TR) of the model, and then applying the model checking algorithm to verify a given formula. In many cases, the full TR is too big to be computed. This problem is addressed by Beer et al., in xe2x80x9cOn-the-fly Model Checking of RCTL Formulas,xe2x80x9d Proceedings of the Tenth International Conference on Computer Aided Verification (CAV 1998), which is incorporated here in by reference. In this paper, the authors describe a technique for solving CTL formulas of the form AG(p) on the fly, wherein p is a Boolean expression. On-the-fly model checking effectively partitions the TR in such a way as to eliminate the large expenditure of computation resources needed to compute the full TR.
An AG(p) formula states that p is true in every reachable state of the model. Therefore, to disprove this formula, it is sufficient to find one xe2x80x9cbadxe2x80x9d state in which p is false. On-the-fly model checking is based on the realization that if S is the set of states in which p is false, then in order to find a bad state, it is necessary only to intersect S with the set of reachable states R, and check that the intersection is not empty. Finding this intersection is computationally easy. It can therefore can be performed on the fly, i.e., after each iteration of a reachability analysis used to find R, rather than waiting until the entire extent of R has been determined. If the intersection of S and R is found at any point to be non-empty, the iterations are stopped, and AG(p) is false. A counterexample is then produced by tracing backward from the intersection region, through the states found in the iterations of the reachability analysis, back to one of the initial states. As long as no intersection is found, the process continues until the entire reachable state space has been computed, so that AG(p) is shown to be true. Thus, there is no need to compute the full transition relation. Furthermore, since counterexamples are produced on the fly, only a portion of the reachable state space must be computed when the formula fails, saving even more time and memory space.
In the above-mentioned article, Beer et al. also define a specification language RCTL, as an extension to the conventional CTL language using regular expressions, which makes it possible to translate many CTL formulas conveniently into state machines having an error state. Such formulas can then be verified by on-the-fly model checking of the formula AG(error). More recently, Beer et al. have extended RCTL to include further expressions and syntax that are useful in creating formulas for on-the-fly model checking, as described in xe2x80x9cThe Temporal Logic Sugar,xe2x80x9d Proceedings of the Thirteenth International Conference on Computer Aided Verification (CAV 2001), which is incorporated here in by reference.
Typically, the most time-consuming step in the process of on-the-fly model checking is computing the next set of states at each iteration of the reachability analysis. (These sets can be seen as a set of concentric rings in state space, and are therefore referred to as xe2x80x9cdonuts.xe2x80x9d) It is desirable to save these donuts for reuse in producing a counterexample trace in case the tested formula is found to be false, in order to avoid having to compute all the donuts twice. Saving all the donuts for such reuse can work well for small-size models.
For model checking of large designs, however, the demand on computer resources involved in saving and maintaining all the donuts is so great that it can cause memory explosion and slow the progress of the model checker to a near standstill. As a result, model checking runs in which the tested formula is found to be true (so that no counterexample exists) are typically completed much faster when the donuts found in the reachability analysis are not saved. When the tested formula is found to be false, however, all the donuts must be recomputed in order to produce a counterexample. This recomputation is a major waste of time and effort. Therefore, neither the approach of saving all the donuts during the reachability analysis nor that of discarding all of them makes optimal use of model checker resources.
In response to this difficulty, preferred embodiments of the present invention provide a method for controlling the amount of memory used to store the donuts during the reachability analysis, so that the model checker runs at optimal speed even on very large models. In these preferred embodiments, a subset of the donuts found in the reachability analysis is saved, while the remaining donuts, between the donuts that are selected to be saved, are discarded. Preferably, a donut is saved once in every n iterations of the reachability analysis, wherein n is an adjustable parameter. When the tested formula is found to be false, and a counterexample must be produced, the saved donuts are used in reconstructing the donuts between them that were previously discarded.
The reconstruction of the donuts and tracing of the counterexample are preferably carried out piece by piece. This process begins with the group of donuts between the last donut that was saved and the final donut, which was found to intersect the target states, and then works backward toward the initial states. After each piece of the counterexample has been traced, the donuts used in producing that piece are discarded, and the next group of donuts is reconstructed. In this manner, memory explosion is avoided, by trading off memory consumption against the added computational burden of recomputing the discarded donuts. The optimal size for n is determined heuristically, based on the size of the design under test and the number of iterations of the transition relation to be used in the reachability analysis, as against the available resources of the model checker.
The methods of the present invention can be used advantageously to find not just a single counterexample trace, but also multiple traces, as described in the above-mentioned U.S. patent application entitled, xe2x80x9cEfficient Production of Disjoint Multiple Traces.xe2x80x9d Furthermore, these methods can be used not only for design verification, to find traces leading to bad states of the system, but also for design exploration, as described in the above-mentioned U.S. patent application Ser. No. 08/362,720.
There is therefore provided, in accordance with a preferred embodiment of the present invention, a method for checking a model, which defines states of a system under study and a transition relation among the states, the method including:
specifying a property that applies to a target set that includes one or more target states among the states of the system under study;
beginning with an initial set of one or more initial states among the states of the system, computing a succession of sets of the states of the system, such that the states in each of the sets are reachable by a successive cycle of the transition relation from the states in a preceding set in the succession;
selecting one or more of the sets in the succession to be saved in a memory, while the sets not selected are discarded;
finding an intersection between one of the sets in the succession and the target set; and
computing a trace from one of the target states in the intersection through the states in the sets in the succession, including the discarded sets, to one of the initial states, using the sets saved in the memory to reconstruct the discarded sets.
Preferably, computing the succession of sets includes determining a first set among the sets in the succession, disjoint from the initial set, such that all of the states in the first set are reached from the initial states in a first cycle of the transition relation, and determining the sets in the succession following the first set, such that all the states in each of the sets are reached from the states in the preceding set in the successive cycle of the transition relation, and so that each of the sets in the succession is disjoint from the initial set and from the other sets determined before it. Typically, computing the trace includes selecting one of the states from each of the successive sets. Most preferably, selecting the one of the states includes, for each of the selected states, choosing a predecessor state among the states in the preceding set until the state on the trace in the first set is found, and choosing the predecessor state in the initial set to the state in the first set.
In a preferred embodiment, selecting the one or more of the sets to be saved includes saving one of the sets in every N sets that are computed in the succession, wherein N is an integer parameter greater than one, and discarding the sets intermediate the saved sets.
Preferably, computing the trace includes:
reconstructing a first group of the discarded sets between an intermediate set among the selected sets and the intersection;
computing a first portion of the trace through the first group of the reconstructed sets;
discarding the first group of the reconstructed sets from the memory;
reconstructing a second group of the discarded sets preceding the intermediate set in the succession;
computing a second portion of the trace through the second group of the reconstructed sets; and
appending the portions of the trace together so as to complete the trace.
Most preferably, reconstructing the first group includes computing the sets in the first group by repeating the step of computing the succession of the sets, starting from the intermediate set. Typically, the second group of the discarded sets includes the discarded sets between a further set among the selected sets, prior to the intermediate set in the succession, and reconstructing the second group includes reconstructing the discarded sets between the further set and the intermediate set in the succession, and the method preferably includes repeating the steps of discarding the reconstructed sets, reconstructing the discarded sets and computing and appending the portions of the trace until the trace reaches one of the initial states.
In a preferred embodiment, specifying the property includes specifying a condition that is expected to be true over all of the reachable states of the system under study, wherein the condition is false in the at least one target state. In another preferred embodiment, specifying the property includes specifying a condition representing a desired behavior of the system under study, such that the condition is fulfilled in the at least one target state.
Preferably, computing the successive reachable sets includes testing the property while computing the sets, and ceasing to compute the sets when the intersection is found. Further preferably, computing the trace includes finding a counterexample to the specified property.
There is also provided, in accordance with a preferred embodiment of the present invention, apparatus for checking a model, which defines states of a system under study and a transition relation among the states, the apparatus including:
a memory, arranged to store data; and
a model processor, which is arranged to receive a property that applies to a target set that includes one or more target states among the states of the system under study, and to compute, beginning with an initial set of one or more initial states among the states of the system, a succession of sets of the states of the system, such that the states in each of the sets are reachable by a successive cycle of the transition relation from the states in a preceding set in the succession, such that while computing the sets, the processor selects one or more of the sets in the succession to be saved in the memory, while the sets not selected are discarded, the processor being further arranged to find an intersection between one of the sets in the succession and the target set, and to compute a trace from one of the target states in the intersection through the states in the sets in the succession, including the discarded sets, to one of the initial states, using the sets saved in the memory to reconstruct the discarded sets.
There is additionally provided, in accordance with a preferred embodiment of the present invention, a computer software product for checking a model, which defines states of a system under study and a transition relation among the states, the product including a computer-readable medium in which program instructions are stored, which instructions, when read by a computer, cause the computer to receive a property that applies to a target set that includes one or more target states among the states of the system under study, and to compute, beginning with an initial set of one or more initial states among the states of the system, a succession of sets of the states of the system, such that the states in each of the sets are reachable by a successive cycle of the transition relation from the states in a preceding set in the succession, such that while computing the sets, the computer selects one or more of the sets in the succession to be saved in the memory, while the sets not selected are discarded, the instructions further causing the computer to find an intersection between one of the sets in the succession and the target set, and to compute a trace from one of the target states in the intersection through the states in the sets in the succession, including the discarded sets, to one of the initial states, using the sets saved in the memory to reconstruct the discarded sets.
The present invention will be more fully understood from the following detailed description of the preferred embodiments thereof, taken together with the drawings in which: